$\forall$$E$:Type, ${\it pred?}$:($E$$\rightarrow$($E$+Unit)), $e$:$E$. $\neg$first($e$) $\Rightarrow$ pred($e$) $\in$ $E$